This PR replaces the encoding of magic wand snapshots for quantified wands as a pair of snaps with a function from snap to snap. The encoding was already updated for non-quantified wands in #836, which fixes an unsoundness when using the same wand in multiple applying-expressions.

There is an existing implementation that also changes the encoding for quantified wands in #849; this PR is intended to replace that existing PR, and it takes some inspiration from it and uses the tests provided by that PR.

The key problem to be solved is that, when working with quantified permissions, Silicon emits additional definitions (e.g. of snapshot maps sm), that can summarize values coming from the left hand side of the wand. These definitions become part of the definition of the wand's snapshot function. So we can get a definition like

forall lhs: Snap :: { mwsf_apply(lhs) } lookup(sm, r) == e(lhs) && ...

When the same wand is applied multiple times with different snapshots, that can lead to contradictions, because lookup(sm, r) is assumed to be equal to both e(lhs1) and e(lhs2), which might be different. The existing PR #849 essentially tried to fix this problem retroactively, rewriting assumed declarations after the fact. This one instead uses (a slightly extended version of) Silicon's existing functionality for extending new declarations like snapshot maps with a number of quantified variables stored in the state, so we get the (unproblematic) version

forall lhs: Snap :: { mwsf_apply(lhs) } lookup(sm(lhs), r) == e(lhs) && ...

Using the existing idea of parameterizing declarations with quantified variables is more in line with the way the existing code works, and minimizes changes, which should enable us to merge some other upcoming wand-related changes more easily.
We do, however, add a new field packagingWandSnapshots to the state instead of using the existing quantifiedVariables field because we want to treat them slightly differently and include them only when absolutely needed.